package control;

import java.io.IOException;
import java.io.PrintWriter;
import java.io.Writer;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.TreeSet;

import javax.swing.JOptionPane;

import data.ActionList;
import data.ProcList;
import data.model.ProcAction;
import data.model.Processor;
import data.model.Task;
import data.model.TaskGraph;
import data.model.TaskGraph.Vertex;

public class Generator {
	
	private static Object[] procArray;
	//private static Object[] actArray;
	private static Task[] taskArray;
	private static ArrayList<Integer> roots;
	private static StringBuilder page;
	private static String ind = "   ";
	private static String mod = "module";
	private static int fin;
	//private static TaskGraph tasks;
	
	private static String scheduleFile = "scheduler.nm";
	
	public static void addScheduleName()
	{
		String s = JOptionPane.showInputDialog(null, "Create schedule name:", "scheduler");
		if(!s.isEmpty())
			scheduleFile = s.replace(" ", "") + ".nm";
	}
		
	public static void runGenerator()
	{

		procArray = ProcList.getList();
		//actArray = ActionList.getList();
		taskArray = TaskGraph.getTaskArray();
		roots = TaskGraph.getRoots();
		
		page = new StringBuilder("pta");
		
		buildTaskModule();
		
		for(Object p : procArray)
			buildProcModule((Processor) p);
				
		buildRewards();
				
		buildLabels();
		
		PrintWriter pr = null;

		try
		{
			//Create printWriter
			pr = new PrintWriter(scheduleFile);

				pr.print(page.toString());

			JOptionPane.showMessageDialog(null,"New scheduler printed.","Done",
					JOptionPane.INFORMATION_MESSAGE);

			pr.close();
			
		}
		//necessary syntax
		catch (IOException io)
		{
			io.printStackTrace();
		}
	}
	
	private static void buildLabels() {
		page.append("\n\n" + "label \"tasks_complete\" = ");
		for(Task t : taskArray)
		{
			page.append(String.format("(%s=%d) & ",t.getConcName(), fin));
		}
		page.delete(page.length() - 3, page.length() );
		page.append(";");
	}

	private static void buildRewards() {
		page.append("\n\n" +"rewards");
		for(Object p : procArray)
		{
			if (!((Processor) p).getProcActions().isEmpty())
			{
				String line = String.format("%s=0 : %f;", ((Processor) p).getConcName(), ((Processor) p).getInactiveCost());
				page.append("\n" + ind + line);
				line = String.format("%s>0 : %f;", ((Processor) p).getConcName(), ((Processor) p).getActiveCost());
				page.append("\n" + ind + line);
			}
		}
		page.append("\n" + "endrewards");
		
	}

	private static void buildTaskModule()
	{
		
		page.append("\n\n" + mod + " scheduler");
		
		buildTaskVariables();
		
		//page.append("\n\n");
		
		buildStartTasks();
		
		buildDoneTasks();
		
		page.append("\n" + "endmodule");

		}
	
	private static void buildDoneTasks()
	{
		for(Object p : procArray)
		{
			int pID = ((Processor) p).getProcID();
			StringBuilder sbd = new StringBuilder();
			StringBuilder sbf = new StringBuilder();
			
			page.append("\n" + ind + "// a task finishes on "+ ((Processor) p).getProcName());
			
			for(Task t : taskArray)
			{
				String task = t.getConcName();
				
				sbd.append("\n" + ind + String.format("[%s_done] %s=%d -> (%s'=%d);",
						((Processor) p).getConcName(), task, pID, task, fin));
				ProcAction pa = ((Processor) p).getProcAction(t.getAction());
				if(pa != null && pa.isFaulty())
					sbf.append("\n" + ind + String.format("[%s_fail] %s=%d -> (%s'=0);",
							((Processor) p).getConcName(), task, pID, task));
			}
			page.append(sbd.toString());
			page.append(sbf.toString() + "\n");		
			
		}
		
	}
	
	private static void buildStartTasks()
	{
		for(Integer id : roots)
		{
			Task t = TaskGraph.getTask(id);
			String task = t.getConcName();
			
			page.append("\n\n" + ind + "// start " + t.getTaskName());
			
			int a = t.getAction();
			String aName = ActionList.getAction(a).getActName();
			
			TreeSet<Integer> procs = ActionList.getAction(a).getProcs();
						
			for(Integer pID : procs)
			{
				page.append("\n" +ind + String.format("[%s_%s] %s=0 -> (%s'=%d);",
						ProcList.getProc(pID).getConcName(), aName, task, task, pID));
			}
			
			//page.append("\n");
		}
		
		for(Task t : taskArray)
		{
			if(!TaskGraph.getDependencies(t.getTaskID()).isEmpty())
			{
				String task = t.getConcName();

				//page.append( "\n" + ind + "// start " + t.getTaskName());

				int a = t.getAction();
				String aName = ActionList.getAction(a).getActName();

				TreeSet<Integer> procs = ActionList.getAction(a).getProcs();

				Iterator<Vertex> it = TaskGraph.getDependencies(t.getTaskID()).iterator();
				StringBuilder sb1 = new StringBuilder(" (must wait for ");
				StringBuilder sb2 = new StringBuilder("");
				while (it.hasNext())
				{
					Task tdep = ((TaskGraph.Vertex) it.next()).getElem();
					sb1.append(tdep.getTaskName() + ", ");
					sb2.append(" & " + "task" + tdep.getTaskID() + "=" + fin);
				}
				sb1.delete(sb1.length() - 2, sb1.length() - 1);
				sb1.append("to complete)");
				String deps1 = sb1.toString();
				String deps2 = sb2.toString();

				page.append("\n\n" + ind + "// start " + t.getTaskName() + deps1);

				for(Integer pID : procs)
				{
					page.append("\n" + ind + String.format("[%s_%s] %s=0%s -> (%s'=%d);",
							ProcList.getProc(pID).getConcName(), aName, task, deps2, task, pID));
					
				}
				
				//page.append("\n");
			}
		}
	}
	
	private static void buildTaskVariables()
	{
		page.append("\n\n" + ind + "//Task status: 0 - not started");

		for(int i = 0; i < procArray.length; i++)
		{
			page.append(", " + ((Processor) procArray[i]).getProcID() + " - on " + ((Processor) procArray[i]).getProcName());
		}

		fin = ((Processor) procArray[procArray.length - 1]).getProcID() + 1;
		page.append(", " + fin + " - finished");
		
		for(Task t : taskArray)
		{
			String task = t.getConcName();
			page.append("\n" + ind + task + " : " + "[0.." + fin + "];");
			if(t.getTaskDesc() != null)
				page.append("	//" + t.getTaskDesc());
		}
	}

	private static void buildProcModule(Processor p)
	{
		if (!p.getProcActions().isEmpty())
		{
			page.append("\n\n" + "// processor: " + p.getProcName() + "\n" + mod + " " + p.getConcName());

			buildProcVariables(p);

			buildInvariants(p);

			buildActions(p);

			page.append("\n\n" + "endmodule");
		}
	}

	private static void buildProcVariables(Processor p ) 
	{
		int done = p.getProcActions().last().getAction() + 1;
		 boolean someFaulty = false; //true if at least one action is faulty
		
		page.append("\n\n" + ind + p.getConcName() + " : [0.." + done + "];  // 0 inactive," );
		
		
		
		for( ProcAction pa : p.getProcActions())
		{
			page.append(" " + pa.getAction() + " - " 
					+ ActionList.getAction(pa.getAction()).getActName() + ",");
		}
		page.append(" " + done + " - done");
		
		for( ProcAction pa : p.getProcActions())
		{
			if (pa.isDelay())
			{
				int[] del = pa.getDelay();
				page.append("\n" + ind + String.format("c%d_%d : [0..%d];", p.getProcID(), pa.getAction(), del[1] - del[0]));
			}
			if (pa.isFaulty())
			{
				someFaulty = true;
			}
			
		}
		
		if (someFaulty)
			{
				page.append("\n" + ind + String.format("fail%d : [0..1];", p.getProcID()));
			}
		page.append("\n" + ind + "x" + p.getProcID() + " : clock; // local clock");

	}
		
	private static void buildInvariants(Processor p )
	{
		int done = p.getProcActions().last().getAction() + 1;
		
		page.append("\n\n" + ind + "invariant");
		
		for( ProcAction pa : p.getProcActions())
		{
			int[] del = pa.getDelay();
			if(!pa.isDelay())
			{
				page.append("\n" + ind + ind + String.format("(%s=%d => x%d<=%d) &",
						p.getConcName(), pa.getAction(), p.getProcID(), del[0]));
			}
			else
			{
				page.append("\n" + ind + ind + String.format("((%s=%d & c%d_%d=0) => x%d<=%d) &",
						p.getConcName(), pa.getAction(), p.getProcID(), pa.getAction(), p.getProcID(),
						del[0]));
				page.append("\n" + ind + ind + String.format("((%s=%d & c%d_%d>0) => x%d<=1) &",
						p.getConcName(), pa.getAction(), p.getProcID(), pa.getAction(), p.getProcID()));
				page.append("\n" + ind + ind + String.format("(%s=%d => x%d<=0) &",
						p.getConcName(), done, p.getProcID()));
			}
		}
		page.delete(page.length() - 1, page.length() );
		page.append("\n" + ind + "endinvariant");
	}
	
	private static void buildActions(Processor p ) {
		 String pName = p.getConcName();
		 int pid = p.getProcID();
		 int done = p.getProcActions().last().getAction() + 1;
		 boolean someFaulty = false; //true if at least one action is faulty
		 boolean someDelay = false; //true if at least one action is delayed

		for( ProcAction pa : p.getProcActions())
		{
			String aName = ActionList.getAction(pa.getAction()).getActName();
			String aDesc = ActionList.getAction(pa.getAction()).getActDesc();		
			
			page.append("\n\n" + ind + "//" + aName);
			if(aDesc != null)
				page.append(" - " + aDesc);
			
			String line = String.format("[%s_%s] (%s=0) -> (%s'=%d) & (x%d'=0); // start",
						pName, aName, pName, pName, pa.getAction(), pid);
				page.append("\n" + ind + line);
				
			if(!pa.isDelay() && !pa.isFaulty())
			{
				line = String.format("[%s_done] (%s=%d) & (x%d=%d) -> (%s'=0) & (x%d'=0); // finish",
						pName, pName, pa.getAction(), pid, pa.getDelay()[0], pName, pid);
				page.append("\n" + ind + line);
			}

			else if(!pa.isDelay() && pa.isFaulty())
			{		
				int[] pf = pa.getFaulty();
				line = String.format("[] (%s=%d) & (x%d=%d) -> %d/%d : (fail%d'=1) & (%s'=%d) & (x%d'=0)" +
						" + %d/%d : (fail%d'=0) & (%s'=%d) & (x%d'=0); // finish",
						pName, pa.getAction(), pid, pa.getDelay()[0], pf[0], pf[1],
						pid, pName, done, pid, pf[1] - pf[0], pf[1], pid,
						pName, done, pid);
				page.append("\n" + ind + line);
				someFaulty = true;
			}
			else if(pa.isDelay() && pa.isFaulty())
			{
				int i =0;
				int[] pd = pa.getDelay();
				int[] pf = pa.getFaulty();
				int xi= pd[0];
				
				for(i = 0; i < pd[2] -1; i++)
				{
					if(i > 0)
						xi = 1; 
					line = String.format("[] (%s=%d) & (c%d_%d=%d) & (x%d=%d) -> %d/%d : (%s'=%d) & (c%d_%d'=0) & (x%d'=0)" +
							" + %d/%d : (%s'=%d) & (c%d_%d'=%d) & (x%d'=0) & (fail%d'=1)" +
							" + %d/%d : (c%d_%d'=%d) & (x%d'=0);",
							pName, pa.getAction(), pid, pa.getAction(), i, pid, xi, pf[0], (pd[2] - i)*pf[1], pName, done, pid, pa.getAction(), pid,
							pf[1] - pf[0], (pd[2] - i)*pf[1], pName, done, pid, pa.getAction(), i, pid, pid, 
							pd[2] - (i + 1), pd[2] - i, pid, pa.getAction(), i + 1, pid);
					page.append("\n" + ind + line);
				}
				line = String.format("[] (%s=%d) & (x%d=1) & (c%d_%d=%d) -> (%s'=%d) & (x%d'=0) & (c%d_%d'=0); // completed",
						pName, pa.getAction(), pid, pid, pa.getAction(), pd[1] - pd[0], pName, done, pid, pid, pa.getAction());
				page.append("\n" + ind + line);
				
				someFaulty = true;
				someDelay = true;
			}
			
			else if(pa.isDelay() && !pa.isFaulty())
			{
				int i =0;
				int[] pd = pa.getDelay();
				int xi= pd[0];
				
				for(i = 0; i < pd[2] -1; i++)
				{
					if(i > 0)
						xi = 1; 
					line = String.format("[] (%s=%d) & (c%d_%d=%d) & (x%d=%d) -> 1/%d : (%s'=%d) & (c%d_%d'=0)" +
							" & (x%d'=0) + %d/%d : (c%d_%d'=%d) & (x%d'=0);",
							pName, pa.getAction(), pid, pa.getAction(), i, pid, xi, pd[2] - i, pName,
							done, pid, pa.getAction(), pid, pd[2] - (i + 1), pd[2] - i, pid, pa.getAction(), i + 1, pid);
					page.append("\n" + ind + line);
				}
				line = String.format("[%s_done] (%s=%d) & (x%d=1) & (c%d_%d=%d) -> (%s'=0) & (x%d'=0) & (c%d_%d'=0); // completed",
						pName, pName, pa.getAction(), pid, pid, pa.getAction(), pd[1] - pd[0], pName, pid, pid, pa.getAction());
				page.append("\n" + ind + line);
				
				someDelay = true;
			}
		}
		
		if(someFaulty)
		{
			String line = String.format("[%s_done] (%s=%d) & (fail%d=0) -> (%s'=0) & (x%d'=0); // completed successfully",
					pName, pName, done, pid, pName, pid);
			page.append("\n\n" + "//done" + "\n" + ind + line);
			line = String.format("[%s_fail] (%s=%d) & (fail%d=1) -> (%s'=0) & (x%d'=0) & (fail%d'=0); // completed with a failure",
					pName, pName, done, pid, pName, pid, pid);
			page.append("\n" + ind + line);
		}
		if(someDelay && !someFaulty)
		{
			String line = String.format("[%s_done] (%s=%d) -> (%s'=0); // completed",
					pName, pName, done, pName);
			page.append("\n\n" + ind + line);
		}
	}
}
